F2F+-decls
== is_req:(E)
==  (is_ack:(E)
==  awaiting:(IdIdId)
==  owes_ack:(IdIdId)
==  C_sub_Id:(ff.C r Id)
==  vbl_locs:(i, j:ff.C. @i(awaiting(i,j):) & @i(owes_ack(i,j):))
==  R_locs:(i:ff.C, e:E. (ff.R(i,e))  (loc(e) = i))
==  req_dcdr:(e:E. Dec(is_req(e)))
==  ack_dcdr:(e:E. Dec(is_ack(e)))
==  R_dcdr:(i:ff.C, e:E. Dec(ff.R(i,e)))
==  S_dcdr:(i, j:ff.C, e:E. Dec(ff.S(i,j,e)))
==  S_locs:(i, j:ff.C, e:E. (ff.S(i,j,e))  (loc(e) = i))
==  (disjoint_msgs:(e:E, sndr, rcvr:ff.C.
==  (disjoint_msgs:([e: sndr is_req rcvr] & [e: rcvr is_ack sndr]))
==  Top)) 

latex

---

clarification:

F2F+-decls{i:l}
F2F+-decls(es; ff)
== is_req:(es-E(es){i})
==  (is_ack:(es-E(es){i})
==  awaiting:(IdIdId)
==  owes_ack:(IdIdId)
==  C_sub_Id:(ff.C r Id)
==  vbl_locs:(i:ff.C, j:ff.C. es-dtype(es;i;awaiting(i,j);) & es-dtype(es;i;owes_ack(i,j);))
==  R_locs:(i:ff.C, e:es-E(es). (ff.R(i,e))  (es-loc(es; e) = i  Id))
==  req_dcdr:(e:es-E(es). Dec(is_req(e)))
==  ack_dcdr:(e:es-E(es). Dec(is_ack(e)))
==  R_dcdr:(i:ff.C, e:es-E(es). Dec(ff.R(i,e)))
==  S_dcdr:(i:ff.C, j:ff.C, e:es-E(es). Dec(ff.S(i,j,e)))
==  S_locs:(i:ff.C, j:ff.C, e:es-E(es). (ff.S(i,j,e))  (es-loc(es; e) = i  Id))
==  (disjoint_msgs:(e:es-E(es).
==  (disjoint_msgs:sndr:ff.C, rcvr:ff.C.
==  (disjoint_msgs:(snd-it(ff;is_req;e;sndr;rcvr) & snd-it(ff;is_ack;e;rcvr;sndr)))
==  Top)) 

latex

Definitions	, x:AB(x), @i(x:T), , ff.R, Dec(P), P  Q, f(a), ff.S, s = t, Id, loc(e), x:A  B(x), E, x:A. B(x), ff.C, A, P & Q, [e: i p j], Top
FDL editor aliases	F2F+-decls